#include <stdio.h>
#include <stdlib.h>
#include <string.h>
#include <setjmp.h>
// Apple: #include <malloc.h>
#include <math.h>
#include <string>
#include <vector>
#include <map>
#include <algorithm>
#include <iostream>

using std::string;
using std::vector;
using std::map;
using namespace std;


int main(int argc, char* argv[]) {
  
  int N;

  if ( argc != 2 ) {
    cout << "Usage: dc-gen <N> " << endl;
    cout << "Where N is the number of cryptographers, > 2" << endl;
    exit(1);
  }
  else {
    N = atoi(argv[1]);
  }
  
  cout << "-- The protocol for the dining cryptographers (Chaum)" <<
    endl <<
    "-- This file is automatically generated for " << N <<
    " cryptographers" << endl;

  cout << "Agent Environment" << endl <<
    "  Obsvars:" << endl <<
    "    numberofodd : { none, even, odd };" << endl << 
    "  end Obsvars" << endl << endl <<
    "  Vars:" << endl;

  /*for (int i=0; i<N; i++) {
    cout << "    coin" << i+1 << " : {head,tail};" << endl;
  }*/
  cout << "  end Vars" << endl << endl <<
    "  RedStates:" << endl <<
    "  end RedStates" << endl << endl;
	
  cout << "  Actions = { none };" << endl <<
    "  Protocol:" << endl <<
    //"    coin1=head : {none};" << endl <<
    "    Other : {none};" << endl <<
    "  end Protocol" << endl << endl;


  // Need to compute when odd and when even for environment
  cout << "  Evolution:" << endl;

  cout << "    numberofodd="<< (N%2==1?"even":"odd") << " if ( ( numberofodd=none) and ( " <<
  endl;
  // assume sayequal=0 and saydifferent=1
  bool firsttime = true;

  for ( int j = 0; j < ( (int)pow(2,N) ) ; j++ ) {
    int nofdiff = 0;
    for ( int k = 0; k < N; k++ ){
      if ( j & ((int)pow(2,k))) {
	nofdiff++;
      }
    }
    if ( !(nofdiff % 2 ) == 0 ) {
      // even combination
      if ( firsttime ) {
	firsttime = false;
      } else {
	cout << "      or " << endl;;
      }
      cout << "( ";
      for ( int k = 0; k < N; k++ ){
	if ( j & ((int)pow(2,k))) {
	  // sayequal
	  cout << " DinCrypt" << k+1 << ".Action=sayequal";
	} else {
	  // saydifferent
	  cout << " DinCrypt" << k+1 << ".Action=saydifferent";
	}
	if ( ! ( k == N-1 ) ) {
	  cout << " and ";
	}
      }
      cout << " ) ";
    }
  }

  cout << ") );" << endl;


  firsttime = true;
  cout << "    numberofodd="<< (N%2==0?"even":"odd") << " if ( ( numberofodd=none) and ( " <<
  endl;
  // assume sayequal=0 and saydifferent=1
  for ( int j = 0; j < ( (int)pow(2,N) ) ; j++ ) {
    int nofdiff = 0;
    for ( int k = 0; k < N; k++ ){
      if ( j & ((int)pow(2,k))) {
	nofdiff++;
      }
    }
    if ( (nofdiff % 2 ) == 0 ) {
      // even combination
      if ( firsttime ) {
	firsttime = false;
      } else {
	cout << "      or " << endl;;
      }

      cout << "( ";
      for ( int k = 0; k < N; k++ ){
	if ( j & ((int)pow(2,k))) {
	  // sayequal
	  cout << " DinCrypt" << k+1 << ".Action=sayequal";
	} else {
	  // saydifferent
	  cout << " DinCrypt" << k+1 << ".Action=saydifferent";
	}
	if ( ! ( k == N-1 ) ) {
	  cout << " and ";
	}
      }
      cout << " ) ";
    }
  }
  cout << " ) );" << endl;

  cout << "  end Evolution" << endl;
  cout << "end Agent" << endl << endl;

  
  for (int i=0; i < N; i++) {
    cout << "Agent DinCrypt" << i+1 << endl;
    cout << "  Vars:" << endl;
    cout << "    payer : {yes,no};" << endl;
    cout << "    coinleft : {head,tail};" << endl;
    cout << "    coinright : {head,tail};" << endl;
    cout << "    seedifferent : { empty, yes, no };" << endl;  		
    cout << "  end Vars" << endl;
  	
    cout << "  RedStates:" << endl;
    cout << "  end RedStates" << endl;
  	
    cout << "  Actions = { sayequal, saydifferent, none };" << endl;
  	
    cout << "  Protocol:" << endl;
    cout << "    (payer=no and seedifferent=yes): {saydifferent};" << endl;
    cout << "    (payer=no and seedifferent=no) : {sayequal};" << endl;
    cout << "    (payer=yes and seedifferent=yes): {sayequal};" << endl;
    cout << "    (payer=yes and seedifferent=no) : {saydifferent};" << endl;
    cout << "    Other: {none};" << endl;
    cout << "  end Protocol" << endl;
  	
    cout << "  Evolution:" << endl;
    cout << "    (seedifferent=no) if ( seedifferent=empty and coinleft=head and coinright=head ) or" << endl;
    cout << "      ( seedifferent=empty and coinleft=tail and coinright=tail ); " << endl;
    cout << "    (seedifferent=yes)  if ( seedifferent=empty and coinleft=head and coinright=tail ) or" << endl;
    cout << "      ( seedifferent=empty and coinleft=tail and coinright=head );" << endl;
    cout << "  end Evolution" << endl;

    cout << "end Agent" << endl;
  }


  cout << "Evaluation" << endl;
  for ( int i=0; i < N; i++ ) {
    cout << "  c"<<i+1<<"paid if ( DinCrypt"<<i+1<<".payer=yes );" << endl;
  }
  cout << "  odd if ( Environment.numberofodd=odd);" << endl;
  cout << "  even if ( Environment.numberofodd=even);" << endl;
  cout << "end Evaluation" << endl;
  
  
  cout << "InitStates" << endl;
  // First who's the payer
  cout << " ( ";
  for (int i=0; i<=N; i++) {
    cout << "(";
    for (int j=0; j<N; j++) {
      cout << "(DinCrypt"<<j+1<<".payer=";
      if ( i==j ) {
	cout << "yes";
      } else {
	cout << "no";
      }
      cout << ")";
      if ( !(j==N-1) ) {
	cout << " and ";
      } else {
	cout << ") " ; //<< endl;
	if ( !(i==N) ) cout << " or " << endl;
      }
    }
  }
  cout << " ) and " << endl;


  // Now the coins: N coins, DC1 can see coin1 (his left) and coin N
  // (his right). Din crypt i can see coin i to his left, i-1 to his
  // right. 
  // Assume head=0, tail=1
  cout << " ( " << endl;
  /*for ( int j = 0; j < ( (int)pow(2,N) ) ; j++ ) {

    vector<int> *coins = new vector<int>();
     for ( int k = 0; k < N; k++ ){
       if ( j & ((int)pow(2,k))) {
	 coins->push_back(0);
       } else {
	 coins->push_back(1);
       }
     }

     cout << " ( ";

     // Cryptographer 1:
     //cout << " and DinCrypt1.coinleft=";
     cout << " DinCrypt1.coinleft=";
     if ((*coins)[0]==0) {
       cout << "head";
     } else {
       cout << "tail";
     }
     cout << " and DinCrypt1.coinright=";
     if ((*coins)[N-1]==0) {
       cout << "head";
     } else {
       cout << "tail";
     }

     // all the other cryptographers
     for (int k=1; k<N; k++) {
       cout << " and DinCrypt"<<k+1<<".coinleft=";
       if ((*coins)[k]==0) {
	 cout << "head";
       } else {
       cout << "tail";
       }
       cout << " and DinCrypt"<<k+1<<".coinright=";
       if ((*coins)[k-1]==0) {
	 cout << "head";
       } else {
	 cout << "tail";
       }       
     }

     cout << " ) ";
     if ( j != (int)pow(2,N)-1 ) {
       cout << " or ";
     }
     cout << endl;
     }*/
  for ( int j = 1; j <= N ; j++ ) {
    int k= (j==N) ? 1 : j+1;
    cout << "!(DinCrypt" << j << ".coinleft=tail and DinCrypt" << k << ".coinright=head) and " <<
      "!(DinCrypt" << j << ".coinleft=head and DinCrypt" << k << ".coinright=tail)";
    if(j<N)
      cout << " and " << endl;
  }
  cout << " ) " << endl;

  cout << " and (Environment.numberofodd=none) " << endl;
  for ( int k=0; k<N; k++ ) {
    cout << " and (DinCrypt"<<k+1<<".seedifferent=empty)";
  }
  cout << ";" << endl;

  cout << "end InitStates" << endl;

  cout << "Groups" << endl;
  //cout << "  g1 = {DinCrypt1,DinCrypt2,DinCrypt3};" << endl;
  cout << "end Groups" << endl;

  cout << "Fairness" << endl;
  cout << "end Fairness" << endl;

  cout << "Formulae"<< endl;
  /*cout << "AG( (odd and !c1paid) -> (K(DinCrypt1,(c2paid";
  for (int k=2; k<N; k++) {
    cout << " or c"<<k+1<<"paid";
  }
  cout << ") ) )";
  for (int k=1; k<N; k++) {
    cout << " and !K(DinCrypt1,c"<<k+1<<"paid)";
  }
  cout << " );" << endl;*/
  /*for(int j=1; j<=N; j++) {
    cout << "AG( (odd and !c" << j << "paid) -> (K(DinCrypt" << j <<",(";
    bool flag = false;
    for (int k=1; k<=N; k++) {
      if(k!=j) {
	if(flag)
	  cout << " or ";
	cout << "c"<<k<<"paid";
	flag = true;
      }
    }
    cout << ") ) )" << endl;
    
    for (int k=1; k<=N; k++) 
      if(j!=k) {
	cout << " and !K(DinCrypt" << j << ",c"<<k<<"paid)";
      }
    cout << " )" <<endl << (j==N ? ";" : "and") << endl;
    }*/
  cout << "  AG("; 
  bool first = true;
  for(int i=1; i<=N; i++) 
    for(int j=1; j<=N; j++) 
      if(i!=j) {
	if(!first)
	  cout << " and" << endl << "     ";
	cout << "!K(DinCrypt" << i <<", c" << j << "paid)";
	first = false;
      }
  cout << ");" << endl;
 
  //cout << "  AG (odd -> c1paid);" << endl;
  cout << "end Formulae" << endl;

}

